notebook.community

Edit and run

Calchylus - Lambda calculus with Hy



$$\Huge Ο’ = πœ†x.(πœ†y.x \space (y \space y)) \space (πœ†y.x \space (y \space y))$$

Calchylus is a combination of Hy macro and Lambda term dictionary. It was written to help to write and evaluate Lambda expressions.

[Lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. - wikipedia.org

The short πœ† macro presented below, makes it possible to define and evaluate Lambda expressions the most conventional way. There is really not much to implement because Hy is already a LISP language. LISP, on the other hand, can be defined as an untyped Lambda calculus extended with constants. So actually we just need to introduce πœ† macro, simplify the usual LISP notation, and act only with functions.

At the current development stage, Calchylus does not provide alpha and beta reduction stages of the terms, just direct evaluation.

Repository

Calchylus Jupyter notebook document and GitHub repository was initialized by Marko Manninen, 08/2017.

Lambda (πœ†) macro





InΒ [1]:



    


; index-find function needs to be available at compile time for the lambda expression macro
(eval-and-compile
  ; set comma constant for separator
  ; at the moment Hy doesn't support dot on macro expressions because dot is mixed with internal HyCons functionality
  ; causing this error: https://github.com/hylang/hy/blob/e8ffd412028232cc2cc4fe4bfb10f21ce8ab2565/hy/compiler.py#L2478
  (setv comma 'Β·)
  ; find index of the element from the list. if the element is not found, return -1
  (defn index-find [elm lst]
    (try (.index lst elm) (except [ValueError] -1))))
; lambda expression macro
(defmacro πœ† [&rest expr]
  (setv idx (index-find comma expr))
  `(fn ~(cut expr 0 (if (pos? idx) idx 0)) ~@(cut expr (inc idx))))



    


















    
Out[1]:








<function _hy_anon_fn_2 at 0x000001F41A7E56A8>

Basics

Syntax

Parentheses ( ) to elaborate function scope, group terms, prevent disambiguity, and wrap application. Lambda symbol πœ† to mark the beginning of the function. Dot separator Β· to distinct function arguments and function body from each other.

Terms

  1. Lambda variables. Any symbol following Hy definitions are accepted. For example single character variable names like x and y, multi character names args, also with capitals FUNC, are allowed.

  2. Lambda abstraction. For example (πœ† x Β· x) creates a definition of the function (fn [x] x), or $x \mapsto x$ in mathematic notation.

  3. Lambda application. For example ((πœ† x Β· x) 1) calls for anonymous function with input value 1.

Lambda abstraction

Lambda abstraction is a function definition similar to this:

$$\Large(πœ† \space x Β· x)$$

We can examine the generated Hy code of the functions with macroexpand:





InΒ [2]:



    


(macroexpand '(πœ† x Β· x))



    


















    
Out[2]:








('fn' ['x'] 'x')

Lambda application

Lambda application is the procedure to evaluate declared functions with a given input. Applications are similar to this:

$$\Large((πœ† \space x Β· x)\space y) \implies y$$

where the first x is a name of the argument of the function. The second x is the return value of the function. y is the input value passed to the function. Later in the document we will use $\implies$ character to denote, if lambda term reduces to simpler terms or if application evaluates to a certain value.

Let us next utilize above application and pass an argument to so called identity function.

Identity function

The identity function returns same value that is passed to the function as an argument. Next we run the simple application of the identity function with the input value 1:





InΒ [3]:



    


((πœ† x Β· x) 1) ; ((πœ† x Β· x) 1) ≑ 1



    


















    
Out[3]:








1

Output is as expected, not very exciting one.

Function as an argument

Argument passed to the function can also be yet another function. Say, we want to pass the identity function to the identity function instead of the static value, then the appication would look this:

$$\Large((πœ† \space x Β· x) \space (πœ† \space x Β· x)) \implies (πœ† \space x Β· x)$$

The outcome of such application is a function, thus it alone cannot evaluate to any value. Rather we need to treat it as a function part of the application and provide input for it:





InΒ [4]:



    


(((πœ† x Β· x) (πœ† x Β· x)) 1)



    


















    
Out[4]:








1

Again output is expected to be 1 because first we pass identity function a to the identity function b and then we pass the value 1 to the identity function b.

Self application

One more step toward deeper nested structures is to call function inside a function:

$$\Large((πœ† \space x \space Β· ((πœ† \space x \space Β· x) \space x)) \space 1) \implies 1$$ 




InΒ [5]:



    


((πœ† x Β· ((πœ† x Β· x) x)) 1)



    


















    
Out[5]:








1

We can see how the result is same in all three examples.

Note also how variable names are same on nested functions. This works because of safe scoping in Hy, but one might understand functionality more clear if different variable names were used like this:

$$\Large(πœ† \space x \space Β· ((πœ† \space y \space Β· y) \space x))$$

Currying

Restriction of the traditional Lambda calculus is that it allows one and only one argument per function. Programmers on most of the modern languages are used to multiary functions. There is a way to imitate multiple argument passing with a nested structure called currying in Lambda calculus.

$$\Large(πœ† \space x \space Β· (πœ† \space y \space Β· (πœ† \space z \space Β· x \space y \space z)))$$

Let us make a simple multiplication with two variables for instance:





InΒ [6]:



    


((((πœ† x Β· (πœ† y Β· (πœ† z Β· (* x y z)))) 2) 2) 2)



    


















    
Out[6]:








8

Many arguments

Also multiple arguments can be passed to the lambda function althought the original specification allows one and only one argument to be passed to the Lambda function.

Support for both zero and multiple arguments simpifies the Lambda expression notation.





InΒ [7]:



    


((πœ† x y z Β· (* x y z)) 2 2 2)



    


















    
Out[7]:








8

Constants

Whatever is the argument, return 1:





InΒ [8]:



    


((πœ† x Β· 2) 1)



    


















    
Out[8]:








2

No arguments?!

In original Lambda Calculus functions must have one and only one argument. Lambda macro in Calchylus is not that restricted. We can omit argument for simplicity:





InΒ [9]:



    


((πœ† Β· 2))



    


















    
Out[9]:








2

Apply function

Further abstracting functional properties of the lambda expressions, we can implement function caller (apply func args) with the next statement:





InΒ [10]:



    


(((πœ† func Β· (πœ† arg Β· (func arg))) (πœ† x Β· x)) 2)



    


















    
Out[10]:








2

















InΒ [11]:



    


(, ((πœ† x Β· x) 1) ((πœ† x Β· x) 2) ((πœ† x Β· x) 3))



    


















    
Out[11]:








(1, 2, 3)

Make pair

$$\Large(πœ† \space x Β· (πœ† \space y Β· (πœ† \space f Β· ((f \space x) \space y))))$$

Select first:





InΒ [12]:



    


((((πœ† x Β· (πœ† y Β· (πœ† f Β· ((f x) y)))) 1) 2) (πœ† x Β· (πœ† y Β· x)))



    


















    
Out[12]:








1

Select second:





InΒ [13]:



    


((((πœ† x Β· (πœ† y Β· (πœ† f Β· ((f x) y)))) 1) 2) (πœ† x Β· (πœ† y Β· y)))



    


















    
Out[13]:








2

Twiddle

Swap function argument pair.





InΒ [14]:



    


; ask for the second but because arguments are swapped, the first one is returned
((((πœ† x Β· (πœ† y Β· (πœ† f Β· ((f y) x)))) 1) 2) (πœ† x Β· (πœ† y Β· y)))



    


















    
Out[14]:








1

Infinite recursion

Produce infinite loop:





InΒ [15]:



    


(try
 ; we will catch recursion error from this line, otherwise output would be messier
 ((πœ† x Β· (x x)) (πœ† x Β· (x x)))
 (except (e RecursionError)
   (print "Eternal loop achieved!")))



    


















    






Eternal loop achieved!

Free and bound variables

Lambda abstractions can hold any free variables, but at the application evaluation, none of the functions should have free variables or it will cause variable definition error. For example, this is ok since we are declaring the function, not executing it:





InΒ [16]:



    


(πœ† x Β· (+ x y))



    


















    
Out[16]:








<function <lambda> at 0x000001F41A8C3268>

But unbound variable y will become a problem on evaluation of the application:





InΒ [17]:



    


(try 
  ((πœ† x Β· (+ x y)) 1)
  (except (e NameError)
    (print e)))



    


















    






name 'y' is not defined

Composition

http://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/lambda-calculus-handout.pdf

Numerals

Addition

Logical operations

Boolean TRUE

Boolean true operator is defined by functional means with a pair selector that returns the first item of the given arguments:

$$\Large(((πœ† \space x Β· (πœ† \space y Β· x)) \space a) \space b) \implies a$$ 




InΒ [18]:



    


; select the first
(((πœ† x Β· (πœ† y Β· x)) 1) 2)



    


















    
Out[18]:








1

Boolean FALSE

Boolean false operator is defined with a pair selector that returns the second item of the given arguments:

$$\Large(((πœ† \space x Β· (πœ† \space y Β· y)) \space a) \space b) \implies b$$ 




InΒ [19]:



    


; select the second
(((πœ† x Β· (πœ† y Β· y)) 1) 2)



    


















    
Out[19]:








2

Conditions

IF-THEN-ELSE condition can be formed with boolean true / false selectors. As we defined earlier, true selector returns the first given argument, and false selector returns the second argument. Thus in Lambda calculus we can produce IF-THEN-ELSE functionality by passing either true or false selector to the function and let it select between the first options and the second option.

Let proposition P be the boolean selector, a the first option, and b the second option. Formal definition of the IF-THEN-ELSE Lambda term would be:

$$\Large(πœ† \space P Β· (πœ† \space a Β· (πœ† \space b Β· ((P \space a) \space b))))$$

In the next example P is $(πœ† \space x Β· (πœ† \space y Β· x))$ (i.e. true), a is literal T, and b is literal F:





InΒ [20]:



    


((((πœ† P Β· (πœ† a Β· (πœ† b Β· ((P a) b)))) (πœ† x Β· (πœ† y Β· x))) 'T) 'F)



    


















    
Out[20]:








'T'

Or with a shorter notation, this time P is $(πœ† \space x Β· (πœ† \space y Β· y))$ (i.e. false):





InΒ [21]:



    


((πœ† P a b Β· (P a b)) (πœ† x y Β· y) 'T 'F)



    


















    
Out[21]:








'F'

Connectives

NOT

$$\Large(πœ† x Β· ((x (πœ† x Β· (πœ† y Β· y))) (πœ† x Β· (πœ† y Β· x))))$$ 




InΒ [22]:



    


((((πœ† x Β· ((x (πœ† x Β· (πœ† y Β· y))) (πœ† x Β· (πœ† y Β· x)))) (πœ† x Β· (πœ† y Β· x))) 'T) 'F)



    


















    
Out[22]:








'F'

















InΒ [23]:



    


(((πœ† x Β· (x (πœ† x y Β· y) (πœ† x y Β· x))) (πœ† x y Β· y)) 'T 'F)



    


















    
Out[23]:








'T'

AND

$$\Large(πœ† a Β· (πœ† b Β· ((a b) (πœ† x Β· (πœ† y Β· y)))))$$ 




InΒ [24]:



    


; IF a is TRUE AND b is TRUE, THEN x, ELSE y
; a is TRUE, b is TRUE, x is T, y is F -> T
(((((πœ† a Β· (πœ† b Β· ((a b) (πœ† x Β· (πœ† y Β· y))))) (πœ† x Β· (πœ† y Β· x))) (πœ† x Β· (πœ† y Β· x))) 'T) 'F)



    


















    
Out[24]:








'T'

















InΒ [25]:



    


(((πœ† a b Β· (a b (πœ† x y Β· y))) (πœ† x y Β· x) (πœ† x y Β· y)) 'T 'F)



    


















    
Out[25]:








'F'

OR

$$\Large(πœ† a Β· (πœ† b Β· ((a (πœ† x Β· (πœ† y Β· x))) b)))$$ 




InΒ [26]:



    


; IF a is TRUE OR b is TRUE, THEN x, ELSE y
; a is TRUE, b is FALSE, x is T, y is F -> T
(((((πœ† a Β· (πœ† b Β· ((a (πœ† x Β· (πœ† y Β· x))) b))) (πœ† x Β· (πœ† y Β· x))) (πœ† x Β· (πœ† y Β· y))) 'T) 'F)



    


















    
Out[26]:








'T'

















InΒ [27]:



    


(((πœ† a b Β· (a (πœ† x y Β· x) b)) (πœ† x y Β· y) (πœ† x y Β· y)) 'T 'F)



    


















    
Out[27]:








'F'

Y combinator

Triangular number

Summation...





InΒ [28]:



    


; loop until given limit and sum up all values -> (summa 10)
; x = function, y = steps, z = result
((πœ† x y Β· (x x y 0)) (πœ† x y z Β· (if (> y 0) (x x (- y 1) (+ y z)) z)) 10)



    


















    
Out[28]:








55

Factorial

Implementing the traditional Y combinator.

$$\Large Ο’ = (πœ† \space x Β· ((πœ† \space y Β· (x \space (y \space y))) \space (πœ† \space y Β· (x \space (y \space y)))))$$ 




InΒ [29]:



    


; loop until given limit and sum up all values -> (product 7)
; x = function, y = steps, z = result
((πœ† x y Β· (x x y 1)) (πœ† x y z Β· (if (> y 0) (x x (- y 1) (* y z)) z)) 7)



    


















    
Out[29]:








5040

















InΒ [30]:



    


;Ξ»t.(Ξ»x.t (x x)) (Ξ»x.t (x x))
;(((πœ† x Β· ((πœ† y Β· (x (y y))) (πœ† y Β· (x (y y))))) (πœ† f Β· (πœ† n Β· (if (= n 1) 1 (* n (f (dec n))))))) 7)
;(((fn [f] ((fn [x] (x x)) (fn [x] (f (fn [y] ((x x) y)))))) (fn [f] (fn [n] (if (< n 3) n (* n (f (dec n))))))) 5)
(((πœ† f Β· ((πœ† x Β· (x x)) (πœ† x Β· (f (πœ† y Β· ((x x) y)))))) (πœ† f Β· (πœ† n Β· (if (< n 3) n (* n (f (dec n))))))) 5)



    


















    
Out[30]:








120

Lists

The MIT License

Copyright (c) 2017 Marko Manninen

Content source: markomanninen/calchylus

Similar notebooks:

notebook.community | gallery | about